Left Termination proof of /tmp/tmp7VELVH/p.pl

Left Termination of the query pattern p(b) w.r.t. the given Prolog program could successfully be proven:

↳ PROLOG

  ↳ PrologToPiTRSProof

p₁(.₂(X, {}₀)).
p₁(.₂(s₁²(X), .₂(Y, Xs))) :- p₁(.₂(X, .₂(Y, Xs))), p₁(.₂(s₁⁴(Y), Xs)).
p₁(.₂(0₀, Xs)) :- p₁(Xs).

With regard to the inferred argument filtering the predicates were used in the following modes:
p₁: (b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

p_1_in_g₁(._2₂(X, []_0)) -> p_1_out_g₁(._2₂(X, []_0))
p_1_in_g₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> if_p_1_in_1_g₄(X, Y, Xs, p_1_in_g₁(._2₂(X, ._2₂(Y, Xs))))
p_1_in_g₁(._2₂(0_0, Xs)) -> if_p_1_in_3_g₂(Xs, p_1_in_g₁(Xs))
if_p_1_in_3_g₂(Xs, p_1_out_g₁(Xs)) -> p_1_out_g₁(._2₂(0_0, Xs))
if_p_1_in_1_g₄(X, Y, Xs, p_1_out_g₁(._2₂(X, ._2₂(Y, Xs)))) -> if_p_1_in_2_g₄(X, Y, Xs, p_1_in_g₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs)))
if_p_1_in_2_g₄(X, Y, Xs, p_1_out_g₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs))) -> p_1_out_g₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs)))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

p_1_in_g₁(._2₂(X, []_0)) -> p_1_out_g₁(._2₂(X, []_0))
p_1_in_g₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> if_p_1_in_1_g₄(X, Y, Xs, p_1_in_g₁(._2₂(X, ._2₂(Y, Xs))))
p_1_in_g₁(._2₂(0_0, Xs)) -> if_p_1_in_3_g₂(Xs, p_1_in_g₁(Xs))
if_p_1_in_3_g₂(Xs, p_1_out_g₁(Xs)) -> p_1_out_g₁(._2₂(0_0, Xs))
if_p_1_in_1_g₄(X, Y, Xs, p_1_out_g₁(._2₂(X, ._2₂(Y, Xs)))) -> if_p_1_in_2_g₄(X, Y, Xs, p_1_in_g₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs)))
if_p_1_in_2_g₄(X, Y, Xs, p_1_out_g₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs))) -> p_1_out_g₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs)))

P_1_IN_G₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> IF_P_1_IN_1_G₄(X, Y, Xs, p_1_in_g₁(._2₂(X, ._2₂(Y, Xs))))
P_1_IN_G₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> P_1_IN_G₁(._2₂(X, ._2₂(Y, Xs)))
P_1_IN_G₁(._2₂(0_0, Xs)) -> IF_P_1_IN_3_G₂(Xs, p_1_in_g₁(Xs))
P_1_IN_G₁(._2₂(0_0, Xs)) -> P_1_IN_G₁(Xs)
IF_P_1_IN_1_G₄(X, Y, Xs, p_1_out_g₁(._2₂(X, ._2₂(Y, Xs)))) -> IF_P_1_IN_2_G₄(X, Y, Xs, p_1_in_g₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs)))
IF_P_1_IN_1_G₄(X, Y, Xs, p_1_out_g₁(._2₂(X, ._2₂(Y, Xs)))) -> P_1_IN_G₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs))

The TRS R consists of the following rules:

p_1_in_g₁(._2₂(X, []_0)) -> p_1_out_g₁(._2₂(X, []_0))
p_1_in_g₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> if_p_1_in_1_g₄(X, Y, Xs, p_1_in_g₁(._2₂(X, ._2₂(Y, Xs))))
p_1_in_g₁(._2₂(0_0, Xs)) -> if_p_1_in_3_g₂(Xs, p_1_in_g₁(Xs))
if_p_1_in_3_g₂(Xs, p_1_out_g₁(Xs)) -> p_1_out_g₁(._2₂(0_0, Xs))
if_p_1_in_1_g₄(X, Y, Xs, p_1_out_g₁(._2₂(X, ._2₂(Y, Xs)))) -> if_p_1_in_2_g₄(X, Y, Xs, p_1_in_g₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs)))
if_p_1_in_2_g₄(X, Y, Xs, p_1_out_g₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs))) -> p_1_out_g₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs)))

The argument filtering Pi contains the following mapping:
p_1_in_g₁(x1) = p_1_in_g₁(x1)
._2₂(x1, x2) = ._2₂(x1, x2)
[]_0 = []_0
s_1₁(x1) = s_1₁(x1)
0_0 = 0_0
p_1_out_g₁(x1) = p_1_out_g
if_p_1_in_1_g₄(x1, x2, x3, x4) = if_p_1_in_1_g₃(x2, x3, x4)
if_p_1_in_3_g₂(x1, x2) = if_p_1_in_3_g₁(x2)
if_p_1_in_2_g₄(x1, x2, x3, x4) = if_p_1_in_2_g₁(x4)
IF_P_1_IN_2_G₄(x1, x2, x3, x4) = IF_P_1_IN_2_G₁(x4)
IF_P_1_IN_3_G₂(x1, x2) = IF_P_1_IN_3_G₁(x2)
IF_P_1_IN_1_G₄(x1, x2, x3, x4) = IF_P_1_IN_1_G₃(x2, x3, x4)
P_1_IN_G₁(x1) = P_1_IN_G₁(x1)

We have to consider all (P,R,Pi)-chains

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

P_1_IN_G₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> IF_P_1_IN_1_G₄(X, Y, Xs, p_1_in_g₁(._2₂(X, ._2₂(Y, Xs))))
P_1_IN_G₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> P_1_IN_G₁(._2₂(X, ._2₂(Y, Xs)))
P_1_IN_G₁(._2₂(0_0, Xs)) -> IF_P_1_IN_3_G₂(Xs, p_1_in_g₁(Xs))
P_1_IN_G₁(._2₂(0_0, Xs)) -> P_1_IN_G₁(Xs)
IF_P_1_IN_1_G₄(X, Y, Xs, p_1_out_g₁(._2₂(X, ._2₂(Y, Xs)))) -> IF_P_1_IN_2_G₄(X, Y, Xs, p_1_in_g₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs)))
IF_P_1_IN_1_G₄(X, Y, Xs, p_1_out_g₁(._2₂(X, ._2₂(Y, Xs)))) -> P_1_IN_G₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs))

The TRS R consists of the following rules:

p_1_in_g₁(._2₂(X, []_0)) -> p_1_out_g₁(._2₂(X, []_0))
p_1_in_g₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> if_p_1_in_1_g₄(X, Y, Xs, p_1_in_g₁(._2₂(X, ._2₂(Y, Xs))))
p_1_in_g₁(._2₂(0_0, Xs)) -> if_p_1_in_3_g₂(Xs, p_1_in_g₁(Xs))
if_p_1_in_3_g₂(Xs, p_1_out_g₁(Xs)) -> p_1_out_g₁(._2₂(0_0, Xs))
if_p_1_in_1_g₄(X, Y, Xs, p_1_out_g₁(._2₂(X, ._2₂(Y, Xs)))) -> if_p_1_in_2_g₄(X, Y, Xs, p_1_in_g₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs)))
if_p_1_in_2_g₄(X, Y, Xs, p_1_out_g₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs))) -> p_1_out_g₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs)))

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

P_1_IN_G₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> IF_P_1_IN_1_G₄(X, Y, Xs, p_1_in_g₁(._2₂(X, ._2₂(Y, Xs))))
IF_P_1_IN_1_G₄(X, Y, Xs, p_1_out_g₁(._2₂(X, ._2₂(Y, Xs)))) -> P_1_IN_G₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs))
P_1_IN_G₁(._2₂(0_0, Xs)) -> P_1_IN_G₁(Xs)
P_1_IN_G₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> P_1_IN_G₁(._2₂(X, ._2₂(Y, Xs)))

The TRS R consists of the following rules:

p_1_in_g₁(._2₂(X, []_0)) -> p_1_out_g₁(._2₂(X, []_0))
p_1_in_g₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> if_p_1_in_1_g₄(X, Y, Xs, p_1_in_g₁(._2₂(X, ._2₂(Y, Xs))))
p_1_in_g₁(._2₂(0_0, Xs)) -> if_p_1_in_3_g₂(Xs, p_1_in_g₁(Xs))
if_p_1_in_3_g₂(Xs, p_1_out_g₁(Xs)) -> p_1_out_g₁(._2₂(0_0, Xs))
if_p_1_in_1_g₄(X, Y, Xs, p_1_out_g₁(._2₂(X, ._2₂(Y, Xs)))) -> if_p_1_in_2_g₄(X, Y, Xs, p_1_in_g₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs)))
if_p_1_in_2_g₄(X, Y, Xs, p_1_out_g₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs))) -> p_1_out_g₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs)))

The argument filtering Pi contains the following mapping:
p_1_in_g₁(x1) = p_1_in_g₁(x1)
._2₂(x1, x2) = ._2₂(x1, x2)
[]_0 = []_0
s_1₁(x1) = s_1₁(x1)
0_0 = 0_0
p_1_out_g₁(x1) = p_1_out_g
if_p_1_in_1_g₄(x1, x2, x3, x4) = if_p_1_in_1_g₃(x2, x3, x4)
if_p_1_in_3_g₂(x1, x2) = if_p_1_in_3_g₁(x2)
if_p_1_in_2_g₄(x1, x2, x3, x4) = if_p_1_in_2_g₁(x4)
IF_P_1_IN_1_G₄(x1, x2, x3, x4) = IF_P_1_IN_1_G₃(x2, x3, x4)
P_1_IN_G₁(x1) = P_1_IN_G₁(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPPoloProof

Q DP problem:
The TRS P consists of the following rules:

P_1_IN_G₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> IF_P_1_IN_1_G₃(Y, Xs, p_1_in_g₁(._2₂(X, ._2₂(Y, Xs))))
IF_P_1_IN_1_G₃(Y, Xs, p_1_out_g) -> P_1_IN_G₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs))
P_1_IN_G₁(._2₂(0_0, Xs)) -> P_1_IN_G₁(Xs)
P_1_IN_G₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> P_1_IN_G₁(._2₂(X, ._2₂(Y, Xs)))

The TRS R consists of the following rules:

p_1_in_g₁(._2₂(X, []_0)) -> p_1_out_g
p_1_in_g₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> if_p_1_in_1_g₃(Y, Xs, p_1_in_g₁(._2₂(X, ._2₂(Y, Xs))))
p_1_in_g₁(._2₂(0_0, Xs)) -> if_p_1_in_3_g₁(p_1_in_g₁(Xs))
if_p_1_in_3_g₁(p_1_out_g) -> p_1_out_g
if_p_1_in_1_g₃(Y, Xs, p_1_out_g) -> if_p_1_in_2_g₁(p_1_in_g₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs)))
if_p_1_in_2_g₁(p_1_out_g) -> p_1_out_g

The set Q consists of the following terms:

p_1_in_g₁(x0)
if_p_1_in_3_g₁(x0)
if_p_1_in_1_g₃(x0, x1, x2)
if_p_1_in_2_g₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_P_1_IN_1_G₃, P_1_IN_G₁}.
By using a polynomial ordering, the following set of Dependency Pairs of this DP problem can be strictly oriented.

P_1_IN_G₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> IF_P_1_IN_1_G₃(Y, Xs, p_1_in_g₁(._2₂(X, ._2₂(Y, Xs))))
P_1_IN_G₁(._2₂(0_0, Xs)) -> P_1_IN_G₁(Xs)

The remaining Dependency Pairs were at least non-strictly be oriented.

IF_P_1_IN_1_G₃(Y, Xs, p_1_out_g) -> P_1_IN_G₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs))
P_1_IN_G₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> P_1_IN_G₁(._2₂(X, ._2₂(Y, Xs)))

With the implicit AFS there is no usable rule.

Used ordering: POLO with Polynomial interpretation:

POL(0_0) = 0
POL(._2₂(x₁, x₂)) = 1 + x₂
POL(IF_P_1_IN_1_G₃(x₁, x₂, x₃)) = 1 + x₂
POL(if_p_1_in_2_g₁(x₁)) = 0
POL(s_1₁(x₁)) = 0
POL(if_p_1_in_1_g₃(x₁, x₂, x₃)) = 0
POL(if_p_1_in_3_g₁(x₁)) = 0
POL([]_0) = 0
POL(p_1_in_g₁(x₁)) = 0
POL(p_1_out_g) = 0
POL(P_1_IN_G₁(x₁)) = x₁

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPPoloProof

                    ↳ QDP

                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF_P_1_IN_1_G₃(Y, Xs, p_1_out_g) -> P_1_IN_G₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs))
P_1_IN_G₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> P_1_IN_G₁(._2₂(X, ._2₂(Y, Xs)))

The TRS R consists of the following rules:

p_1_in_g₁(._2₂(X, []_0)) -> p_1_out_g
p_1_in_g₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> if_p_1_in_1_g₃(Y, Xs, p_1_in_g₁(._2₂(X, ._2₂(Y, Xs))))
p_1_in_g₁(._2₂(0_0, Xs)) -> if_p_1_in_3_g₁(p_1_in_g₁(Xs))
if_p_1_in_3_g₁(p_1_out_g) -> p_1_out_g
if_p_1_in_1_g₃(Y, Xs, p_1_out_g) -> if_p_1_in_2_g₁(p_1_in_g₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs)))
if_p_1_in_2_g₁(p_1_out_g) -> p_1_out_g

The set Q consists of the following terms:

p_1_in_g₁(x0)
if_p_1_in_3_g₁(x0)
if_p_1_in_1_g₃(x0, x1, x2)
if_p_1_in_2_g₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {P_1_IN_G₁, IF_P_1_IN_1_G₃}.
The approximation of the Dependency Graph contains 1 SCC with 1 less node.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPPoloProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

P_1_IN_G₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> P_1_IN_G₁(._2₂(X, ._2₂(Y, Xs)))

The TRS R consists of the following rules:

p_1_in_g₁(._2₂(X, []_0)) -> p_1_out_g
p_1_in_g₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> if_p_1_in_1_g₃(Y, Xs, p_1_in_g₁(._2₂(X, ._2₂(Y, Xs))))
p_1_in_g₁(._2₂(0_0, Xs)) -> if_p_1_in_3_g₁(p_1_in_g₁(Xs))
if_p_1_in_3_g₁(p_1_out_g) -> p_1_out_g
if_p_1_in_1_g₃(Y, Xs, p_1_out_g) -> if_p_1_in_2_g₁(p_1_in_g₁(._2₂(s_1₁(s_1₁(s_1₁(s_1₁(Y)))), Xs)))
if_p_1_in_2_g₁(p_1_out_g) -> p_1_out_g

The set Q consists of the following terms:

p_1_in_g₁(x0)
if_p_1_in_3_g₁(x0)
if_p_1_in_1_g₃(x0, x1, x2)
if_p_1_in_2_g₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {P_1_IN_G₁}.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, we can delete all non-usable rules from R.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPPoloProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

P_1_IN_G₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> P_1_IN_G₁(._2₂(X, ._2₂(Y, Xs)))

R is empty.
The set Q consists of the following terms:

p_1_in_g₁(x0)
if_p_1_in_3_g₁(x0)
if_p_1_in_1_g₃(x0, x1, x2)
if_p_1_in_2_g₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {P_1_IN_G₁}.
We used the following order and afs together with the size-change analysis to show that there are no infinite chains for this DP problem.

Order:Homeomorphic Embedding Order

AFS:
s_1₁(x1) = s_1₁(x1)
._2₂(x1, x2) = x1

From the DPs we obtained the following set of size-change graphs:

P_1_IN_G₁(._2₂(s_1₁(s_1₁(X)), ._2₂(Y, Xs))) -> P_1_IN_G₁(._2₂(X, ._2₂(Y, Xs))) (allowed arguments on rhs = {1})
The graph contains the following edges 1 > 1

We oriented the following set of usable rules. none